/FONT#0=BDB30
␈↓␈↓FOL Project 1 Feb 1974
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
TASK DESCRIPTION #1
␈↓ ↓H

␈↓ ↓H
DECISION PROCEDURE FOR THE ALGEBRA OF SETS AND SOME OTHER ALGEBRAIC SYSTEMS
␈↓ ↓H

␈↓ ↓H

␈↓ ↓H
␈↓ α This␈α∞is␈α∞the␈α∞first␈α∞of␈α∞a␈α
series␈α
of␈α
memos␈α
describing␈α
some␈α
improvements␈α
that␈α
need␈α
to␈α
be
␈↓ ↓Hmade␈α⊂to␈α⊂FOL.␈α⊂The␈α⊂purpose␈α⊂of␈α⊂the␈α⊂memos␈α⊂is␈α⊂to␈α⊂aid␈α⊂in␈α⊂dividing␈α⊂up␈α⊂the␈α⊂work␈α⊂and␈α∂to␈α∂make
␈↓ ↓Hpossible␈αconsensus␈αon␈αwhat␈αthe␈αimprovements␈αshould␈αbe.

␈↓ α The␈α
algebra␈αof␈αsets␈αis␈αa␈αpart␈αof␈αset␈αtheory␈αnot␈αinvolving␈αthe␈αε␈αrelation.␈αIn␈αits␈αsimplest
␈↓ ↓Hform␈α∩it␈α∩involves␈α∩the␈α∩operations␈α∩∪␈α∩(union),␈α∩∩␈α∩(intersection)␈α∩and␈α∩~␈α⊃(complementation␈α⊃with
␈↓ ↓Hrespect␈αto␈αa␈αuniversal␈αset␈αUSET).␈αThe␈αfollowing␈αare␈αuniversally␈αvalid␈αformulas:

␈↓ ↓H
␈↓ α 1. x ∪ (y ∪ z) = (x ∪ y) ∪ z associativity
␈↓ ↓H
␈↓ α 2. x ∩ (y ∩ z) = (x ∩ y) ∩ z
␈↓ ↓H
␈↓ α 3. x ∩ (y ∩ z) = (x ∩ y) ∪ (x ∩ z)
␈↓ ↓H
␈↓ α 4. x ∪ (y ∩ z) = (x ∪ y) ∩ (x ∪ z)
␈↓ ↓H
␈↓ α 5. x ∩ x = x
␈↓ ↓H
␈↓ α 6. x ∪ x = x
␈↓ ↓H
␈↓ α 7. ~(x ∪ y) = ~x ∩ ~y
␈↓ ↓H
␈↓ α 8. ~(x ∩ y = ~x ∪ ~y
␈↓ ↓H
␈↓ α 9. ~~x = x
␈↓ ↓H
␈↓ α 10. ~NLSET = USET
␈↓ ↓H
␈↓ α 11. ~USET = NLSET
␈↓ ↓H
␈↓ α 12. x ∪ NLSET = x
␈↓ ↓H
␈↓ α 13. x ∩ NLSET = NLSET
␈↓ ↓H
␈↓ α 14. x ∪ USET = USET
␈↓ ↓H
␈↓ α 15. x ∩ USET = x.
␈↓ ↓H

␈↓ ↓H
␈↓ α These␈αlaws␈αare␈αidentical␈αto␈αlaws␈αof␈αthe␈αpropositional␈αcalculus␈αwith␈α∨,␈α∧,␈α¬,␈α≡,␈αfalse,␈αand
␈↓ ↓Htrue␈αreplacing␈α∪,␈α∩,␈α~,␈α=,␈αNLSET,␈αand␈αUSET␈αrespectively.

␈↓ α Therefore,␈α∂the␈α∂program␈α∂taut,␈α∂already␈α∂part␈α∂of␈α∂FOL,␈α∂can␈α∂be␈α∞used␈α∞to␈α∞decide␈α∞whether␈α∞a
␈↓ ↓Hformula␈α⊃involving␈α⊃these␈α⊃operators␈α⊂follows␈α⊂by␈α⊂Boolean␈α⊂algebra␈α⊂from␈α⊂a␈α⊂collection␈α⊂of␈α⊂other
␈↓ ↓Hformulas.␈α
All␈α
that␈α
is␈α
required␈α
is␈α
a␈α
program␈α
that␈α
translates␈αthe␈αBoolean␈αformulas␈αinto␈αlogical
␈↓ ↓Hformulas␈α∞and␈α∞uses␈α
taut.␈α
(Indeed,␈α
if␈α
only␈α
the␈α
Boolean␈α
operations␈α
were␈α
to␈α
be␈α
used,␈α
one␈α
would
␈↓ ↓Hnot␈αwant␈αboth␈αthe␈αBoolean␈αan␈αpropositional␈αoperators).

␈↓ α There␈α∂is␈α∂one␈α∂minor␈α∂embarassment␈α∂that␈α∂is␈α∂easily␈α∂fixed.␈α∂While␈α∂the␈α∞universal␈α∞set␈α∞USET
␈↓ ↓Hleads␈α∞to␈α∞no␈α∞trouble␈α∞in␈α∞Boolean␈α∞algebra␈α
and␈α
is␈α
a␈α
convenient␈α
fiction,␈α
in␈α
conjunction␈α
with␈α
the
␈↓ ↓Hother␈α∞axioms␈α∞and␈α∞operations␈α∞of␈α
ZF,␈α
it␈α
leads␈α
to␈α
a␈α
contradiction.␈α
Therefore␈α
it␈α
is␈α
necesary␈α
to
␈↓ ↓Hreplace␈αthe␈αcomplementation␈αoperation␈α~␈αby␈αa␈αset␈αdifference␈αoperation␈αand␈αget␈αrid␈αof␈αUSET.
␈↓ ↓HWe␈α∀can␈α∀write␈α∀setdiff(x,y)␈α∀or␈α∀x\y␈α∀(or␈α∀even␈α∀x␈α∪-␈α∪y␈α∪if␈α∪the␈α∪sort␈α∪features␈α∪of␈α∪FOL␈α∪can␈α∪be
␈↓ ↓Hstraightened␈αout␈αto␈αpermit␈αusing␈α-␈αfor␈αboth␈αsets␈αand␈αnumbers).␈αWe␈αcan␈αstill␈αuse␈αtaut;␈αwe␈αhave
␈↓ ↓Honly␈αto␈αtranslate␈αsetdiff(x,y)␈αinto␈αx∧¬y.

␈↓ α Therefore,␈α⊂we␈α⊂can␈α⊂have␈α⊂a␈α⊂rule␈α⊂booltaut␈α∂in␈α∂FOL␈α∂that␈α∂will␈α∂let␈α∂us␈α∂assert␈α∂any␈α∂formula
␈↓ ↓Hthat␈α
follows␈α
by␈αBoolean␈αalgebra␈αfrom␈αa␈αcollection␈αof␈αlines␈αof␈αthe␈αproof␈αor␈αaxioms␈αor␈αstored
␈↓ ↓Htheorems.␈α∪As␈α∪with␈α∪propositional␈α∪formulas,␈α∪the␈α∩Boolean␈α∩formulas␈α∩can␈α∩involve␈α∩other␈α∩than
␈↓ ↓HBoolean␈αoperators,␈αexpressions␈αinvolving␈αthese␈αother␈αoperators␈αbeing␈αtreated␈αas␈αatoms␈αin␈αthe
␈↓ ↓HBoolean␈αalgebra.

␈↓ α However,␈αbooltaut␈αneeds␈αsome␈αsyntactic␈αsugar,␈αnamely

␈↓ α 1.␈αSince␈α∪␈αand␈α∩␈αare␈αassociative,␈αwe␈αneed␈αto␈αbe␈αable␈αto␈αwrite␈αx␈α∪␈αy␈α∪␈αz,␈αetc.

␈↓ α 2.␈α
Instead␈α
of␈α
writing␈α
only␈α
equalities,␈α
we␈αwant␈αalso␈αto␈αuse␈αthe␈αinclusion␈αsymbol␈α⊂.␈αThis
␈↓ ↓His␈αhandled␈αby␈αtranslating␈αx␈α⊂␈αy␈αinto␈αx␈α⊃␈αy.

␈↓ α 3.␈α∀We␈α∀need␈α∀the␈α∀operator␈α∀{x,y,...,z}␈α∀for␈α∀explicitly␈α∀listed␈α∪sets.␈α∪This␈α∪can␈α∪be␈α∪done␈α∪by
␈↓ ↓Hregarding␈α{x,y,...,z}␈αas␈αan␈αabbreviation␈αfor␈αunitset(x)␈α∪␈αunitset(y)␈α∪␈α...␈αunitset(z).

␈↓ α 4.␈αExpressions␈αof␈αthe␈αform␈αx␈αε␈αA␈αcan␈αbe␈αallowed␈αin␈αthe␈αformulas␈αby␈αtransforming␈αthem
␈↓ ↓Hinto␈αunitset(x)␈α⊂␈αA.

␈↓ α 5.␈α→Conjunctions␈α_of␈α_Boolean␈α_algebra␈α_formulas␈α_can␈α_be␈α_allowed␈α_in␈α_premisses␈α_and
␈↓ ↓Hconclusions␈αsince␈αthe␈αprogram␈αcan␈αreplace␈αthem␈αby␈αa␈αnumber␈αof␈αseparate␈αformulas.

␈↓ α Besides␈αthese␈αfeatures␈αwhich␈αcan␈αbe␈αadded␈αwithout␈αchanging␈αthe␈αreliance␈αon␈αtaut,␈αthere
␈↓ ↓Hare␈α
some␈α
possible␈α
extensions␈α
that␈α
may␈αrequire␈αadditional␈αmathematics␈αto␈αdetermine␈αwhether
␈↓ ↓Hthe␈α⊂domain␈α⊂is␈α⊂still␈α⊂decidable␈α⊂and␈α⊂whether␈α⊂decision␈α⊂procedures␈α⊂are␈α⊂feasible.␈α∂Here␈α∂are␈α∂some
␈↓ ↓Hpossibilities:

␈↓ α 1.␈α∩Can␈α∩we␈α∩allow␈α∩other␈α∩propositional␈α∩combinations␈α∩of␈α∩the␈α∩Boolean␈α∩formulas␈α⊃in␈α⊃the
␈↓ ↓Hpremisses␈αand␈αconclusions?␈αThis␈αseems␈αto␈αrequire␈αat␈αleast␈αthe␈αelementary␈αtheory␈αof␈αequality.

␈↓ α 2.␈αCan␈αwe␈αinclude␈αthe␈αCartesian␈αproduct␈αin␈αthe␈αalgebra?

␈↓ ↓H

␈↓ ↓H
OTHER ALGEBRAIC SYSTEMS
␈↓ ↓H

␈↓ ↓H
␈↓ α 1.␈α∀Associativity.␈α∀Certain␈α∀operators␈α∪are␈α∪associative,␈α∪and␈α∪if␈α∪we␈α∪can't␈α∪write␈α∪them␈α∪in
␈↓ ↓Hbinary␈α∞form,␈α∞proofs␈α
of␈α
certain␈α
equivalences␈α
can␈α
be␈α
quite␈α
tedious.␈α
It␈α
would␈α
be␈α
best␈α
if␈α
having
␈↓ ↓Hproved␈α∂an␈α∂operator␈α∂associative,␈α∂we␈α∂could␈α∂write␈α∂it␈α∂without␈α∂grouping␈α∂the␈α∞terms␈α∞in␈α∞twos␈α∞and
␈↓ ↓Hmake␈αall␈αdeductions␈αdepending␈αsolely␈αon␈αits␈αassociativity␈αin␈αone␈αstep.

␈↓ α 2.␈αCommutativity.␈αThe␈αprevious␈αremark␈αapplies␈αhere␈αwithout␈αchange.

␈↓ α 3.␈α⊂Distributive␈α⊂pairs␈α⊂of␈α⊂operators.␈α⊂The␈α⊂case␈α⊂where␈α⊂there␈α∂is␈α∂a␈α∂commutative␈α∂operator
␈↓ ↓Hwritten␈α∃additively␈α∀and␈α∀another␈α∀associative␈α∀operator␈α∀which␈α∀obeys␈α∀distributive␈α∀laws␈α∀with
␈↓ ↓Hrespect␈α∂to␈α∂the␈α∂first␈α∂is␈α∂quite␈α∂common.␈α∂Sometimes␈α∞the␈α∞multiplicative␈α∞operator␈α∞is␈α∞distributive
␈↓ ↓Halso.␈α∂In␈α∂these␈α∂cases␈α∂formal␈α∂multiplication␈α∞and␈α∞exponentiation␈α∞by␈α∞integers␈α∞also␈α∞occur.␈α∞There
␈↓ ↓Hare␈α∪a␈α∪number␈α∪of␈α∪cases,␈α∪but␈α∪in␈α∩each␈α∩case,␈α∩informal␈α∩proofs␈α∩make␈α∩heavy␈α∩use␈α∩of␈α∩what␈α∩are
␈↓ ↓Happarently␈αdecision␈αprocedures.

␈↓ ↓H

␈↓ ↓H
FINAL REMARK
␈↓ ↓H

␈↓ ↓H
␈↓ α The␈α⊗possibility␈α∃that␈α∃there␈α∃are␈α∃a␈α∃large␈α∃number␈α∃of␈α∃such␈α∃elementary␈α∃proof␈α∃search
␈↓ ↓Hprocedures␈α∞that␈α∞will␈α∞have␈α∞to␈α
be␈α
added␈α
to␈α
FOL␈α
to␈α
make␈α
proofs␈α
as␈α
short␈α
as␈α
informal␈α
ones␈α
is
␈↓ ↓Hsomewhat␈α
daunting.␈α
Perhaps␈α
there␈α
is␈α
a␈α
general␈α
way␈α
of␈α
adding␈αthe␈αpossibility␈αof␈αproof␈αsearch
␈↓ ↓Hprocedures␈αto␈αFOL␈αsimply␈αby␈αreading␈αin␈αfiles.